Theorem 3expia 1122

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ad5ant125  1369  mp3an3  1453  3gencl  3473  vtocl3gaf  3524  vtocl3ga  3526  moi  3664  disji  5070  disjord  5074  3optocl  5728  sossfld  6150  f1oresrab  7080  f1cdmsn  7237  soisores  7282  isomin  7292  isofrlem  7295  ovmpos  7515  ov2gf  7516  ndmovord  7557  nnsuc  7835  poxp  8078  frpoins3xp3g  8091  brtpos  8185  dfsmo2  8287  smoiun  8301  smoord  8305  smogt  8307  omeulem1  8517  omeu  8520  oewordi  8527  uniinqs  8744  mapvalg  8783  pmvalg  8784  elmapg  8786  xpdom3  9013  mapdom3  9087  sdomdomtrfi  9135  domsdomtrfi  9136  php  9141  php3  9143  nndomog  9147  onomeneq  9148  sucdom  9154  unxpdomlem3  9168  isinf  9175  f1finf1o  9183  isfinite2  9208  prfi  9234  ordiso  9431  cnfcom3clem  9626  r111  9699  tskwe  9874  pr2ne  9927  infxpenlem  9935  dfac8alem  9951  infdif  10130  infdif2  10131  cff1  10180  coflim  10183  cfslbn  10189  cfslb2n  10190  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  fin23lem27  10250  isf32lem9  10283  isf34lem6  10302  axcc2lem  10358  domtriomlem  10364  axdc4lem  10377  zorn2lem2  10419  axdclem2  10442  konigthlem  10491  gchen1  10548  gchen2  10549  gchpwdom  10593  gchaleph  10594  winainflem  10616  tskcard  10704  gruiun  10722  gruen  10735  intgru  10737  grudomon  10740  grur1a  10742  grutsk1  10744  nqereu  10852  nqereq  10858  ltsonq  10892  prlem934  10956  reclem3pr  10972  1re  11144  axsup  11221  addlid  11329  recex  11782  lemul1a  12009  lt2msq  12041  fimaxre2  12101  indpi1  12173  zdiv  12599  zextlt  12603  prime  12610  uzind2  12622  fzind  12627  lbzbi  12886  qbtwnxr  13152  qextltlem  13154  xralrple  13157  xltneg  13169  xlt2add  13212  supxrgtmnf  13281  ixxub  13319  ixxlb  13320  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  iocssre  13380  icossre  13381  iccssre  13382  fzen  13495  expclzlem  14045  expaddz  14068  expmulz  14070  hashgadd  14339  hashunsngx  14355  hashgt23el  14386  elovmpowrd  14520  pfxnd0  14651  ccatopth2  14679  pfxccatin12  14695  cshf1  14772  shftuz  15031  cau3lem  15317  caubnd  15321  climuni  15514  lo1resb  15526  o1resb  15528  o1of2  15575  o1add  15576  o1mul  15577  o1sub  15578  ntrivcvgmul  15867  eflt  16084  moddvds  16232  dvdscmulr  16253  dvdsmulcr  16254  dvdsle  16279  divalglem8  16369  divalgb  16373  ndvdssub  16378  bitsfzo  16404  gcdcllem1  16468  gcdcllem3  16470  dvdsgcd  16513  nn0rppwr  16530  nn0expgcd  16533  lcmgcdlem  16575  lcmfeq0b  16599  qredeu  16627  isprm3  16652  prmdvdsexpr  16687  prmexpb  16689  eulerthlem2  16752  fermltl  16754  coprimeprodsq  16779  pythagtrip  16805  pcprendvds  16811  pcpremul  16814  pcdvdsb  16840  pc2dvds  16850  4sqlem12  16927  4sqlem18  16933  vdwlem10  16961  cshwshashlem3  17068  xpsrnbas  17535  ismred  17564  mrieqv2d  17605  iscatd  17639  isfuncd  17832  fthestrcsetc  18116  fthsetcestrc  18131  poslubd  18377  dirtr  18568  mulgaddcom  19074  ghmrn  19204  pmtrprfv3  19429  mndodcongi  19518  oddvdsnn0  19519  oddvds  19522  odcl2  19540  odhash3  19551  gexdvds  19559  pgpfi  19580  lsmss1b  19641  lsmss2b  19643  efgsrel  19709  efgred  19723  cntzcmn  19815  cyggenod  19859  lt6abl  19870  gsumcom2  19950  pgpfac1lem2  20052  pgpfac1lem3  20054  dvdsunit  20359  unitmulclb  20361  irredrmul  20407  isabvd  20789  lmodvsdi  20880  lss0cl  20942  islbs3  21153  lbsextlem2  21157  xrsdsreclblem  21393  psrbaglefi  21906  mvrf1  21964  coe1fzgsumd  22269  gsummoncoe1  22273  evl1gsumd  22322  scmataddcl  22481  scmatsubcl  22482  mdetunilem9  22585  mdetuni0  22586  mdetmul  22588  m2cpmrngiso  22723  pm2mpf1  22764  opnnei  23085  neindisj2  23088  cncls2  23238  cncls  23239  cnntr  23240  cnpresti  23253  cnprest  23254  lmcnp  23269  isreg2  23342  ordthauslem  23348  unconn  23394  2ndc1stc  23416  kgen2ss  23520  ptclsg  23580  cnmptcom  23643  kqfvima  23695  hmeof1o  23729  fbncp  23804  fbfinnfr  23806  trfbas2  23808  isufil2  23873  ufprim  23874  trufil  23875  filufint  23885  hausflim  23946  flimrest  23948  flimcls  23950  cnpfcf  24006  alexsubALT  24016  tmdgsum  24060  opnsubg  24073  cldsubg  24076  qustgpopn  24085  tsmsxp  24120  blpnf  24362  blssps  24389  blss  24390  blssec  24400  neibl  24466  prdsxmslem2  24494  xrsmopn  24778  metnrm  24828  climcncf  24867  iccpnfhmeo  24912  xrhmeo  24913  bndth  24925  cphsqrtcl3  25154  iscau2  25244  iscmet3lem2  25259  bcthlem5  25295  bcth3  25298  ishl2  25337  ivthlem1  25418  cmmbl  25501  iundisj2  25516  voliunlem2  25518  mbfaddlem  25627  itg2itg1  25703  itg2seq  25709  itg2mulclem  25713  cnplimc  25854  dvres2  25879  deg1nn0clb  26055  deg1lt0  26056  deg1ge  26063  plypf1  26177  plyadd  26182  plymul  26183  coeeu  26190  dgrub2  26200  coeidlem  26202  coeid3  26205  coemullem  26215  coe11  26218  coemulhi  26219  coemulc  26220  dgreq0  26230  dgrlt  26231  dgradd2  26233  vieta1lem2  26277  tanord1  26501  tanord  26502  logccne0  26542  cxpeq0  26642  cxpmul2z  26655  cxpcn3lem  26711  rtprmirr  26724  relogbzcl  26738  angpieqvd  26795  o1cxp  26938  scvxcvx  26949  chtublem  27174  bposlem3  27249  lgsqr  27314  2sqnn  27402  dchrisumlema  27451  dchrisumlem2  27453  ostth2lem3  27598  nosepon  27629  noextenddif  27632  nolesgn2o  27635  nogesgn1o  27637  nosepne  27644  nodense  27656  onnolt  28258  onlts  28259  oniso  28263  bdayn0p1  28361  bdayn0sf1o  28362  tghilberti2  28706  inagswap  28909  f1otrg  28939  brbtwn2  28974  axpasch  29010  axcontlem4  29036  axcontlem5  29037  upgredg2vtx  29210  usgredg2vtxeuALT  29291  sizusglecusg  29532  upgredginwlk  29704  frgrwopreg1  30388  frgrwopreg2  30389  frgrregorufrg  30396  lpni  30551  ipasslem5  30906  htthlem  30988  omlsii  31474  spansni  31628  spansneleq  31641  elspansn4  31644  sumspansn  31720  homco1  31872  homulass  31873  mdsl0  32381  ssdmd1  32384  ssdmd2  32385  cvdmd  32408  chirredlem2  32462  atdmd  32469  atmd2  32471  disjif  32648  iundisj2f  32660  isoun  32775  preiman0  32783  padct  32791  iocinioc2  32852  iundisj2fi  32870  sgn3da  32907  sgnnbi  32911  sgnpbi  32912  archiabllem1a  33252  archiabllem2a  33255  slmdvsdi  33276  ordtconnlem1  34068  measinblem  34364  measres  34366  measdivcstALTV  34369  mbfmco2  34409  orvclteinc  34620  bnj605  35049  bnj607  35058  bnj964  35085  bnj1033  35111  bnj1128  35132  bnj1137  35137  bnj1136  35139  bnj1413  35177  bnj60  35204  rankfilimb  35245  r1filim  35247  fineqvac  35260  fineqvnttrclselem3  35267  fineqvnttrclse  35268  cusgredgex  35304  subgrwlk  35314  acycgr1v  35331  cvmlift2lem10  35494  msubvrs  35742  wsuclem  36005  dfrdg4  36133  brcolinear2  36240  brsegle2  36291  nn0prpw  36505  ntruni  36509  clsint2  36511  fnessref  36539  fnemeet2  36549  fnejoin2  36551  limsucncmpi  36627  ee7.2aOLD  36643  bj-idreseq  37476  dissneqlem  37656  isbasisrelowllem1  37671  isbasisrelowllem2  37672  icoreclin  37673  poimirlem9  37950  poimirlem30  37971  poimirlem32  37973  areacirc  38034  filbcmb  38061  mettrifi  38078  heiborlem8  38139  heiborlem10  38141  heibor  38142  riscer  38309  igenval2  38387  eldisjim3  39136  eldisjs6  39261  lshpcmp  39434  eqlkr  39545  lkrlsp2  39549  lkrshp  39551  cvrnbtwn2  39721  cvlexch3  39778  cvlexch4N  39779  cvlatexchb1  39780  cvlsupr3  39790  exatleN  39850  cvratlem  39867  atcvrj2b  39878  cvrat3  39888  cvrat4  39889  athgt  39902  ps-1  39923  ps-2  39924  3atlem5  39933  3at  39936  llnneat  39960  llnmlplnN  39985  lplnneat  39991  lplnnelln  39992  islpln2a  39994  lplnriaN  39996  lplnribN  39997  lplnexllnN  40010  2llnjaN  40012  lvolnle3at  40028  lvolneatN  40034  lvolnelln  40035  lvolnelpln  40036  islvol2aN  40038  dalem62  40180  pmapglb2N  40217  pmapglb2xN  40218  lncmp  40229  paddasslem14  40279  paddasslem15  40280  pmod2iN  40295  hlmod1i  40302  pclfinclN  40396  osumcllem8N  40409  pexmidlem4N  40419  pl42lem1N  40425  pl42lem4N  40428  lhpexle1  40454  lhpexle2lem  40455  lhpmcvr5N  40473  lhpmcvr6N  40474  ltrneq  40595  trlnidatb  40623  cdleme0ex2N  40670  cdleme27a  40813  cdleme17d3  40942  cdlemeg46gfre  40978  cdleme48gfv1  40982  cdlemeg49lebilem  40985  cdlemf2  41008  cdlemf  41009  cdlemfnid  41010  trlord  41015  cdlemg31c  41145  cdlemg35  41159  trlcone  41174  tendoeq2  41220  cdlemj3  41269  cdlemk26b-3  41351  cdlemk33N  41355  cdleml3N  41424  cdlemn  41658  dih1dimb2  41687  dihord5apre  41708  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem2N  41740  dihglblem3N  41741  dihmeetlem13N  41765  dihmeetlem15N  41767  dihatexv  41784  hdmap14lem12  42325  uzindd  42417  lcmineqlem1  42468  sticksstones1  42585  dvdsexpnn0  42766  frlmfzowrdb  42949  oddcomabszz  43372  jm2.19lem4  43420  fiuneneq  43620  idomsubgmo  43621  omcl2  43761  pwinfi3  43990  gneispa  44557  mnringmulrcld  44655  grumnudlem  44712  ismnushort  44728  binomcxplemnn0  44776  addrcom  44901  int3  45039  suctrALT  45252  suctrALTcf  45348  suctrALT3  45350  chordthmALT  45359  iunconnlem2  45361  relpmin  45379  relpfrlem  45380  stoweidlem26  46454  stoweidlem34  46462  issald  46761  goldbachth  48010  nprmdvdsfacm1  48087  grlimgrtri  48479  nnsgrp  48653  ply1mulgsumlem1  48862  lubsscl  49435  glbsscl  49436