Theorem jaod 718

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  719  jaao  720  orel2  727  pm2.621  748  mtord  784  jaodan  798  pm2.63  801  pm2.74  808  dedlema  971  dedlemb  972  oplem1  977  ifnebibdc  3600  opthpr  3798  exmid1stab  4237  trsucss  4454  ordsucim  4532  onsucelsucr  4540  0elnn  4651  xpsspw  4771  relop  4812  fununi  5322  poxp  6285  nntri1  6549  nnsseleq  6554  nnmordi  6569  nnaordex  6581  nnm00  6583  swoord2  6617  nneneq  6913  exmidonfinlem  7253  elni2  7374  prubl  7546  distrlem4prl  7644  distrlem4pru  7645  ltxrlt  8085  recexre  8597  remulext1  8618  mulext1  8631  un0addcl  9273  un0mulcl  9274  elnnz  9327  zleloe  9364  zindd  9435  uzsplit  10158  fzm1  10166  expcl2lemap  10622  expnegzap  10644  expaddzap  10654  expmulzap  10656  qsqeqor  10721  nn0opthd  10793  facdiv  10809  facwordi  10811  bcpasc  10837  recvguniq  11139  absexpzap  11224  maxabslemval  11352  xrmaxiflemval  11393  sumrbdclem  11520  summodc  11526  zsumdc  11527  prodrbdclem  11714  zproddc  11722  prodssdc  11732  fprodcl2lem  11748  fprodsplitsn  11776  ordvdsmul  11977  gcdaddm  12121  nninfctlemfo  12177  lcmdvds  12217  dvdsprime  12260  prmdvdsexpr  12288  prmfac1  12290  pythagtriplem2  12404  4sqlem11  12539  unct  12599  domneq0  13768  baspartn  14218  reopnap  14706  coseq0q4123  14969  lgsdir2lem2  15145  decidin  15289  bj-charfun  15299  bj-nntrans  15443  bj-nnelirr  15445  bj-findis  15471  triap  15519