Theorem jaod 725

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

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  726  jaao  727  orel2  734  pm2.621  755  mtord  791  jaodan  805  pm2.63  808  pm2.74  815  dedlema  978  dedlemb  979  oplem1  984  ifnebibdc  3668  opthpr  3876  exmid1stab  4321  trsucss  4544  ordsucim  4622  onsucelsucr  4630  0elnn  4741  xpsspw  4862  relop  4905  fununi  5424  poxp  6428  nntri1  6729  nnsseleq  6734  nnmordi  6749  nnaordex  6761  nnm00  6763  swoord2  6797  nneneq  7111  exmidonfinlem  7496  elni2  7629  prubl  7801  distrlem4prl  7899  distrlem4pru  7900  ltxrlt  8339  recexre  8852  remulext1  8873  mulext1  8886  un0addcl  9529  un0mulcl  9530  elnnz  9587  zleloe  9624  zindd  9696  uzsplit  10426  fzm1  10434  expcl2lemap  10913  expnegzap  10935  expaddzap  10945  expmulzap  10947  qsqeqor  11012  nn0opthd  11084  facdiv  11100  facwordi  11102  bcpasc  11128  recvguniq  11680  absexpzap  11765  maxabslemval  11893  xrmaxiflemval  11935  sumrbdclem  12063  summodc  12069  zsumdc  12070  prodrbdclem  12257  zproddc  12265  prodssdc  12275  fprodcl2lem  12291  fprodsplitsn  12319  ordvdsmul  12520  gcdaddm  12680  nninfctlemfo  12736  lcmdvds  12776  dvdsprime  12819  prmdvdsexpr  12847  prmfac1  12849  pythagtriplem2  12964  4sqlem11  13099  unct  13193  domneq0  14418  baspartn  14915  reopnap  15411  coseq0q4123  15699  lgsdir2lem2  15902  upgrpredgv  16141  wlk1walkdom  16354  decidin  16569  bj-charfun  16577  bj-nntrans  16721  bj-nnelirr  16723  bj-findis  16749  triap  16813