Theorem jaod 722

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  723  jaao  724  orel2  731  pm2.621  752  mtord  788  jaodan  802  pm2.63  805  pm2.74  812  dedlema  975  dedlemb  976  oplem1  981  ifnebibdc  3648  opthpr  3850  exmid1stab  4292  trsucss  4514  ordsucim  4592  onsucelsucr  4600  0elnn  4711  xpsspw  4831  relop  4872  fununi  5389  poxp  6384  nntri1  6650  nnsseleq  6655  nnmordi  6670  nnaordex  6682  nnm00  6684  swoord2  6718  nneneq  7026  exmidonfinlem  7382  elni2  7512  prubl  7684  distrlem4prl  7782  distrlem4pru  7783  ltxrlt  8223  recexre  8736  remulext1  8757  mulext1  8770  un0addcl  9413  un0mulcl  9414  elnnz  9467  zleloe  9504  zindd  9576  uzsplit  10300  fzm1  10308  expcl2lemap  10785  expnegzap  10807  expaddzap  10817  expmulzap  10819  qsqeqor  10884  nn0opthd  10956  facdiv  10972  facwordi  10974  bcpasc  11000  recvguniq  11521  absexpzap  11606  maxabslemval  11734  xrmaxiflemval  11776  sumrbdclem  11903  summodc  11909  zsumdc  11910  prodrbdclem  12097  zproddc  12105  prodssdc  12115  fprodcl2lem  12131  fprodsplitsn  12159  ordvdsmul  12360  gcdaddm  12520  nninfctlemfo  12576  lcmdvds  12616  dvdsprime  12659  prmdvdsexpr  12687  prmfac1  12689  pythagtriplem2  12804  4sqlem11  12939  unct  13028  domneq0  14251  baspartn  14739  reopnap  15235  coseq0q4123  15523  lgsdir2lem2  15723  upgrpredgv  15959  wlk1walkdom  16100  decidin  16216  bj-charfun  16225  bj-nntrans  16369  bj-nnelirr  16371  bj-findis  16397  triap  16457