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  7274  elni2  7400  prubl  7572  distrlem4prl  7670  distrlem4pru  7671  ltxrlt  8111  recexre  8624  remulext1  8645  mulext1  8658  un0addcl  9301  un0mulcl  9302  elnnz  9355  zleloe  9392  zindd  9463  uzsplit  10186  fzm1  10194  expcl2lemap  10662  expnegzap  10684  expaddzap  10694  expmulzap  10696  qsqeqor  10761  nn0opthd  10833  facdiv  10849  facwordi  10851  bcpasc  10877  recvguniq  11179  absexpzap  11264  maxabslemval  11392  xrmaxiflemval  11434  sumrbdclem  11561  summodc  11567  zsumdc  11568  prodrbdclem  11755  zproddc  11763  prodssdc  11773  fprodcl2lem  11789  fprodsplitsn  11817  ordvdsmul  12018  gcdaddm  12178  nninfctlemfo  12234  lcmdvds  12274  dvdsprime  12317  prmdvdsexpr  12345  prmfac1  12347  pythagtriplem2  12462  4sqlem11  12597  unct  12686  domneq0  13906  baspartn  14394  reopnap  14890  coseq0q4123  15178  lgsdir2lem2  15378  decidin  15551  bj-charfun  15561  bj-nntrans  15705  bj-nnelirr  15707  bj-findis  15733  triap  15786