Theorem jaod 395

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

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 32	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 32	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 394	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385

This theorem is referenced by:  mpjaod  396  orel2  398  pm2.621  424  jaao  531  jaodan  826  pm2.63  829  ecase2d  981  ecase3d  984  dedlema  1002  dedlemb  1003  cad0  1556  psssstr  3713  eqoreldif  4225  opthpr  4384  sotric  5061  sotr2  5064  relop  5272  suctr  5808  trsucss  5811  ordelinel  5825  ordelinelOLD  5826  fununi  5964  fnprb  6472  soisoi  6578  ordunisuc2  7044  poxp  7289  soxp  7290  wfrlem14  7428  wfrlem15  7429  tfrlem11  7484  omordi  7646  om00  7655  odi  7659  omeulem2  7663  oewordi  7671  nnmordi  7711  omsmolem  7733  swoord2  7774  nneneq  8143  dffi3  8337  inf3lem6  8530  cantnfle  8568  cantnflem1  8586  cantnflem2  8587  r1sdom  8637  r1ord3g  8642  rankxplim3  8744  carddom2  8803  wdomnumr  8887  alephordi  8897  alephdom  8904  cardaleph  8912  cdainf  9014  cfsuc  9079  cfsmolem  9092  sornom  9099  fin23lem25  9146  fin1a2lem11  9232  fin1a2s  9236  zorn2lem7  9324  ttukeylem5  9335  alephval2  9394  fpwwe2lem13  9464  gch2  9497  gchaclem  9500  prub  9816  sqgt0sr  9927  1re  10039  lelttr  10128  ltletr  10129  letr  10131  mul0or  10667  prodgt0  10868  mulge0b  10893  squeeze0  10926  sup2  10979  un0addcl  11326  un0mulcl  11327  nn0sub  11343  elnnz  11387  zindd  11478  rpneg  11863  xrlttri  11972  xrlelttr  11987  xrltletr  11988  xrletr  11989  qextlt  12034  qextle  12035  xmullem2  12095  xlemul1a  12118  xrsupexmnf  12135  xrinfmexpnf  12136  supxrun  12146  prunioo  12301  difreicc  12304  iccsplit  12305  uzsplit  12412  fzm1  12420  expcl2lem  12872  expeq0  12890  expnegz  12894  expaddz  12904  expmulz  12906  sqlecan  12971  facdiv  13074  facwordi  13076  bcpasc  13108  resqrex  13991  absexpz  14045  caubnd  14098  summo  14448  zsum  14449  zprod  14667  rpnnen2lem12  14954  ordvdsmul  15022  dvdsprime  15400  prmdvdsexpr  15429  prmfac1  15431  pythagtriplem2  15522  4sqlem11  15659  vdwlem6  15690  vdwlem9  15693  vdwlem13  15697  cshwshashlem3  15804  prmlem0  15812  xpscfv  16222  pleval2  16965  pltletr  16971  plelttr  16972  tsrlemax  17220  f1omvdco2  17868  psgnunilem2  17915  efgredlemc  18158  frgpuptinv  18184  lt6abl  18296  dmdprdsplit2lem  18444  drngmul0or  18768  lvecvs0or  19108  domneq0  19297  baspartn  20758  0top  20787  indistopon  20805  restntr  20986  cnindis  21096  cmpfi  21211  filconn  21687  ufprim  21713  ufildr  21735  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  ovolicc2lem3  23287  rolle  23753  dvivthlem1  23771  coeaddlem  24005  dgrco  24031  plymul0or  24036  aalioulem3  24089  cxpge0  24429  cxpmul2z  24437  cxpcn3lem  24488  scvxcvx  24712  sqf11  24865  ppiublem1  24927  lgsdir2lem2  25051  lgsqrlem2  25072  lmieu  25676  upgrpredgv  26034  edglnl  26038  eucrct2eupth  27105  frgrogt3nreg  27255  nvmul0or  27505  hvmul0or  27882  disjxpin  29401  subfacp1lem4  31165  untsucf  31587  sotr3  31656  dfon2lem6  31693  dftrpred3g  31733  nosepon  31818  nolesgn2ores  31825  nosepne  31831  nolt02o  31845  nosupbnd1lem5  31858  broutsideof2  32229  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  lineunray  32254  lineelsb2  32255  finminlem  32312  nn0prpw  32318  refssfne  32353  meran1  32410  ontgval  32430  ordcmp  32446  bj-sngltag  32971  bj-ismooredr2  33065  topdifinfindis  33194  icoreclin  33205  finxpsuclem  33234  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  mblfinlem2  33447  ovoliunnfl  33451  itg2addnclem  33461  sdclem2  33538  fdc  33541  divrngidl  33827  lkreqN  34457  cvrnbtwn4  34566  4atlem12  34898  elpaddn0  35086  paddasslem17  35122  paddidm  35127  pmapjoin  35138  llnexchb2  35155  dalawlem13  35169  dalawlem14  35170  dochkrshp4  36678  lcfl6  36789  fphpdo  37381  pellfundex  37450  jm2.19lem4  37559  jm2.26a  37567  relexpmulg  38002  relexp01min  38005  relexpxpmin  38009  relexpaddss  38010  clsk1indlem3  38341  goldbachthlem2  41458  evenltle  41626  gbowge7  41651  bgoldbtbndlem3  41695  lidldomn1  41921  uzlidlring  41929