Theorem jaod 717

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 716	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 30	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  718  jaao  719  orel2  726  pm2.621  747  mtord  783  jaodan  797  pm2.63  800  pm2.74  807  dedlema  969  dedlemb  970  oplem1  975  opthpr  3768  trsucss  4417  ordsucim  4493  onsucelsucr  4501  0elnn  4612  xpsspw  4732  relop  4770  fununi  5276  poxp  6223  nntri1  6487  nnsseleq  6492  nnmordi  6507  nnaordex  6519  nnm00  6521  swoord2  6555  nneneq  6847  exmidonfinlem  7182  elni2  7288  prubl  7460  distrlem4prl  7558  distrlem4pru  7559  ltxrlt  7997  recexre  8509  remulext1  8530  mulext1  8543  un0addcl  9182  un0mulcl  9183  elnnz  9236  zleloe  9273  zindd  9344  uzsplit  10062  fzm1  10070  expcl2lemap  10502  expnegzap  10524  expaddzap  10534  expmulzap  10536  qsqeqor  10600  nn0opthd  10670  facdiv  10686  facwordi  10688  bcpasc  10714  recvguniq  10972  absexpzap  11057  maxabslemval  11185  xrmaxiflemval  11226  sumrbdclem  11353  summodc  11359  zsumdc  11360  prodrbdclem  11547  zproddc  11555  prodssdc  11565  fprodcl2lem  11581  fprodsplitsn  11609  ordvdsmul  11809  gcdaddm  11952  lcmdvds  12046  dvdsprime  12089  prmdvdsexpr  12117  prmfac1  12119  pythagtriplem2  12233  unct  12410  baspartn  13119  reopnap  13609  coseq0q4123  13826  lgsdir2lem2  14001  decidin  14109  bj-charfun  14119  bj-nntrans  14263  bj-nnelirr  14265  bj-findis  14291  exmid1stab  14310  triap  14338