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  3605  opthpr  3803  exmid1stab  4242  trsucss  4459  ordsucim  4537  onsucelsucr  4545  0elnn  4656  xpsspw  4776  relop  4817  fununi  5327  poxp  6299  nntri1  6563  nnsseleq  6568  nnmordi  6583  nnaordex  6595  nnm00  6597  swoord2  6631  nneneq  6927  exmidonfinlem  7272  elni2  7398  prubl  7570  distrlem4prl  7668  distrlem4pru  7669  ltxrlt  8109  recexre  8622  remulext1  8643  mulext1  8656  un0addcl  9299  un0mulcl  9300  elnnz  9353  zleloe  9390  zindd  9461  uzsplit  10184  fzm1  10192  expcl2lemap  10660  expnegzap  10682  expaddzap  10692  expmulzap  10694  qsqeqor  10759  nn0opthd  10831  facdiv  10847  facwordi  10849  bcpasc  10875  recvguniq  11177  absexpzap  11262  maxabslemval  11390  xrmaxiflemval  11432  sumrbdclem  11559  summodc  11565  zsumdc  11566  prodrbdclem  11753  zproddc  11761  prodssdc  11771  fprodcl2lem  11787  fprodsplitsn  11815  ordvdsmul  12016  gcdaddm  12176  nninfctlemfo  12232  lcmdvds  12272  dvdsprime  12315  prmdvdsexpr  12343  prmfac1  12345  pythagtriplem2  12460  4sqlem11  12595  unct  12684  domneq0  13904  baspartn  14370  reopnap  14866  coseq0q4123  15154  lgsdir2lem2  15354  decidin  15527  bj-charfun  15537  bj-nntrans  15681  bj-nnelirr  15683  bj-findis  15709  triap  15760