Theorem jaod 669

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))

Assertion

Ref	Expression
jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 30	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 30	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 668	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 30	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpjaod  670  jaao  671  orel2  677  pm2.621  698  mtord  729  jaodan  743  pm2.63  746  pm2.74  753  dedlema  910  dedlemb  911  oplem1  916  opthpr  3564  trsucss  4178  ordsucim  4244  onsucelsucr  4252  0elnn  4358  xpsspw  4468  relop  4504  fununi  4987  poxp  5873  nntri1  6097  nnsseleq  6102  nnmordi  6112  nnaordex  6123  nnm00  6125  swoord2  6159  nneneq  6343  elni2  6504  prubl  6676  distrlem4prl  6774  distrlem4pru  6775  ltxrlt  7178  recexre  7678  remulext1  7699  mulext1  7712  un0addcl  8321  un0mulcl  8322  elnnz  8361  zleloe  8398  zindd  8465  uzsplit  9109  fzm1  9117  expcl2lemap  9488  expnegzap  9510  expaddzap  9520  expmulzap  9522  nn0opthd  9649  facdiv  9665  facwordi  9667  bcpasc  9693  recvguniq  9881  absexpzap  9966  maxabslemval  10094  ordvdsmul  10236  gcdaddm  10375  lcmdvds  10461  dvdsprime  10504  prmdvdsexpr  10529  prmfac1  10531  bj-nntrans  10746  bj-nnelirr  10748  bj-findis  10774