Theorem 3expia 1120

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

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

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 206  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant125  1365  mp3an3  1449  3gencl  3517  moi  3714  disji  5131  disjord  5136  3optocl  5772  sossfld  6185  f1oresrab  7127  f1cdmsn  7283  soisores  7327  isomin  7337  isofrlem  7340  ovmpos  7559  ov2gf  7560  ndmovord  7601  nnsuc  7877  poxp  8119  frpoins3xp3g  8132  brtpos  8226  dfsmo2  8353  smoiun  8367  smoord  8371  smogt  8373  omeulem1  8588  omeu  8591  oewordi  8597  uniinqs  8797  mapvalg  8836  pmvalg  8837  elmapg  8839  xpdom3  9076  mapdom3  9155  sdomdomtrfi  9210  domsdomtrfi  9211  php  9216  php3  9218  nndomog  9222  php3OLD  9230  onomeneq  9234  sucdom  9241  unxpdomlem3  9258  isinf  9266  isinfOLD  9267  f1finf1o  9277  findcard2OLD  9290  isfinite2  9307  ordiso  9517  cnfcom3clem  9706  r111  9776  tskwe  9951  pr2ne  10005  pr2neOLD  10006  infxpenlem  10014  dfac8alem  10030  infdif  10210  infdif2  10211  cff1  10259  coflim  10262  cfslbn  10268  cfslb2n  10269  cofsmo  10270  cfsmolem  10271  cfcoflem  10273  fin23lem27  10329  isf32lem9  10362  isf34lem6  10381  axcc2lem  10437  domtriomlem  10443  axdc4lem  10456  zorn2lem2  10498  axdclem2  10521  konigthlem  10569  gchen1  10626  gchen2  10627  gchpwdom  10671  gchaleph  10672  winainflem  10694  tskcard  10782  gruiun  10800  gruen  10813  intgru  10815  grudomon  10818  grur1a  10820  grutsk1  10822  nqereu  10930  nqereq  10936  ltsonq  10970  prlem934  11034  reclem3pr  11050  1re  11221  axsup  11296  addlid  11404  recex  11853  lemul1a  12075  lt2msq  12106  fimaxre2  12166  zdiv  12639  zextlt  12643  prime  12650  uzind2  12662  fzind  12667  lbzbi  12927  qbtwnxr  13186  qextltlem  13188  xralrple  13191  xltneg  13203  xlt2add  13246  supxrgtmnf  13315  ixxub  13352  ixxlb  13353  ioo0  13356  ico0  13377  ioc0  13378  icc0  13379  iocssre  13411  icossre  13412  iccssre  13413  fzen  13525  expclzlem  14056  expaddz  14079  expmulz  14081  hashgadd  14344  hashunsngx  14360  hashgt23el  14391  elovmpowrd  14515  pfxnd0  14645  ccatopth2  14674  pfxccatin12  14690  cshf1  14767  shftuz  15023  cau3lem  15308  caubnd  15312  climuni  15503  lo1resb  15515  o1resb  15517  o1of2  15564  o1add  15565  o1mul  15566  o1sub  15567  ntrivcvgmul  15855  eflt  16067  moddvds  16215  dvdscmulr  16235  dvdsmulcr  16236  dvdsle  16260  divalglem8  16350  divalgb  16354  ndvdssub  16359  bitsfzo  16383  gcdcllem1  16447  gcdcllem3  16449  dvdsgcd  16493  lcmgcdlem  16550  lcmfeq0b  16574  qredeu  16602  isprm3  16627  prmdvdsexpr  16661  prmexpb  16664  eulerthlem2  16722  fermltl  16724  coprimeprodsq  16748  pythagtrip  16774  pcprendvds  16780  pcpremul  16783  pcdvdsb  16809  pc2dvds  16819  4sqlem12  16896  4sqlem18  16902  vdwlem10  16930  cshwshashlem3  17038  xpsrnbas  17524  ismred  17553  mrieqv2d  17590  iscatd  17624  isfuncd  17822  fthestrcsetc  18112  fthsetcestrc  18127  poslubd  18376  dirtr  18565  mulgaddcom  19021  ghmrn  19150  pmtrprfv3  19370  mndodcongi  19459  oddvdsnn0  19460  oddvds  19463  odcl2  19481  odhash3  19492  gexdvds  19500  pgpfi  19521  lsmss1b  19582  lsmss2b  19584  efgsrel  19650  efgred  19664  cntzcmn  19756  cyggenod  19800  lt6abl  19811  gsumcom2  19891  pgpfac1lem2  19993  pgpfac1lem3  19995  dvdsunit  20277  unitmulclb  20279  irredrmul  20325  isabvd  20659  lmodvsdi  20727  lss0cl  20790  islbs3  21002  lbsextlem2  21006  xrsdsreclblem  21280  psrbaglefi  21795  mvrf1  21856  coe1fzgsumd  22146  gsummoncoe1  22148  evl1gsumd  22196  scmataddcl  22338  scmatsubcl  22339  mdetunilem9  22442  mdetuni0  22443  mdetmul  22445  m2cpmrngiso  22580  pm2mpf1  22621  opnnei  22944  neindisj2  22947  cncls2  23097  cncls  23098  cnntr  23099  cnpresti  23112  cnprest  23113  lmcnp  23128  isreg2  23201  ordthauslem  23207  unconn  23253  2ndc1stc  23275  kgen2ss  23379  ptclsg  23439  cnmptcom  23502  kqfvima  23554  hmeof1o  23588  fbncp  23663  fbfinnfr  23665  trfbas2  23667  isufil2  23732  ufprim  23733  trufil  23734  filufint  23744  hausflim  23805  flimrest  23807  flimcls  23809  cnpfcf  23865  alexsubALT  23875  tmdgsum  23919  opnsubg  23932  cldsubg  23935  qustgpopn  23944  tsmsxp  23979  blpnf  24223  blssps  24250  blss  24251  blssec  24261  neibl  24330  prdsxmslem2  24358  xrsmopn  24648  metnrm  24698  climcncf  24740  iccpnfhmeo  24790  xrhmeo  24791  bndth  24804  cphsqrtcl3  25035  iscau2  25125  iscmet3lem2  25140  bcthlem5  25176  bcth3  25179  ishl2  25218  ivthlem1  25300  cmmbl  25383  iundisj2  25398  voliunlem2  25400  mbfaddlem  25509  itg2itg1  25586  itg2seq  25592  itg2mulclem  25596  cnplimc  25736  dvres2  25761  deg1nn0clb  25946  deg1lt0  25947  deg1ge  25954  plypf1  26064  plyadd  26069  plymul  26070  coeeu  26077  dgrub2  26087  coeidlem  26089  coeid3  26092  coemullem  26102  coe11  26105  coemulhi  26106  coemulc  26107  dgreq0  26118  dgrlt  26119  dgradd2  26121  vieta1lem2  26163  tanord1  26386  tanord  26387  logccne0  26427  cxpeq0  26526  cxpmul2z  26539  cxpcn3lem  26596  relogbzcl  26620  angpieqvd  26677  o1cxp  26820  scvxcvx  26831  chtublem  27057  bposlem3  27132  lgsqr  27197  2sqnn  27285  dchrisumlema  27334  dchrisumlem2  27336  ostth2lem3  27481  nosepon  27511  noextenddif  27514  nolesgn2o  27517  nogesgn1o  27519  nosepne  27526  nodense  27538  tghilberti2  28322  inagswap  28525  f1otrg  28555  brbtwn2  28596  axpasch  28632  axcontlem4  28658  axcontlem5  28659  upgredg2vtx  28834  usgredg2vtxeuALT  28912  sizusglecusg  29153  upgredginwlk  29326  frgrwopreg1  30004  frgrwopreg2  30005  frgrregorufrg  30012  lpni  30166  ipasslem5  30521  htthlem  30603  omlsii  31089  spansni  31243  spansneleq  31256  elspansn4  31259  sumspansn  31335  homco1  31487  homulass  31488  mdsl0  31996  ssdmd1  31999  ssdmd2  32000  cvdmd  32023  chirredlem2  32077  atdmd  32084  atmd2  32086  disjif  32242  iundisj2f  32254  isoun  32356  preiman0  32364  padct  32377  iocinioc2  32423  iundisj2fi  32441  archiabllem1a  32773  archiabllem2a  32776  slmdvsdi  32796  ordtconnlem1  33368  indpi1  33482  measinblem  33682  measres  33684  measdivcstALTV  33687  mbfmco2  33728  orvclteinc  33938  sgn3da  34004  sgnnbi  34008  sgnpbi  34009  bnj605  34382  bnj607  34391  bnj964  34418  bnj1033  34444  bnj1128  34465  bnj1137  34470  bnj1136  34472  bnj1413  34510  bnj60  34537  fineqvac  34561  cusgredgex  34576  subgrwlk  34587  acycgr1v  34604  cvmlift2lem10  34767  msubvrs  35015  wsuclem  35267  dfrdg4  35393  brcolinear2  35500  brsegle2  35551  nn0prpw  35672  ntruni  35676  clsint2  35678  fnessref  35706  fnemeet2  35716  fnejoin2  35718  limsucncmpi  35794  ee7.2aOLD  35810  bj-idreseq  36507  dissneqlem  36685  isbasisrelowllem1  36700  isbasisrelowllem2  36701  icoreclin  36702  poimirlem9  36961  poimirlem30  36982  poimirlem32  36984  areacirc  37045  filbcmb  37072  mettrifi  37089  heiborlem8  37150  heiborlem10  37152  heibor  37153  riscer  37320  igenval2  37398  lshpcmp  38322  eqlkr  38433  lkrlsp2  38437  lkrshp  38439  cvrnbtwn2  38609  cvlexch3  38666  cvlexch4N  38667  cvlatexchb1  38668  cvlsupr3  38678  exatleN  38739  cvratlem  38756  atcvrj2b  38767  cvrat3  38777  cvrat4  38778  athgt  38791  ps-1  38812  ps-2  38813  3atlem5  38822  3at  38825  llnneat  38849  llnmlplnN  38874  lplnneat  38880  lplnnelln  38881  islpln2a  38883  lplnriaN  38885  lplnribN  38886  lplnexllnN  38899  2llnjaN  38901  lvolnle3at  38917  lvolneatN  38923  lvolnelln  38924  lvolnelpln  38925  islvol2aN  38927  dalem62  39069  pmapglb2N  39106  pmapglb2xN  39107  lncmp  39118  paddasslem14  39168  paddasslem15  39169  pmod2iN  39184  hlmod1i  39191  pclfinclN  39285  osumcllem8N  39298  pexmidlem4N  39308  pl42lem1N  39314  pl42lem4N  39317  lhpexle1  39343  lhpexle2lem  39344  lhpmcvr5N  39362  lhpmcvr6N  39363  ltrneq  39484  trlnidatb  39512  cdleme0ex2N  39559  cdleme27a  39702  cdleme17d3  39831  cdlemeg46gfre  39867  cdleme48gfv1  39871  cdlemeg49lebilem  39874  cdlemf2  39897  cdlemf  39898  cdlemfnid  39899  trlord  39904  cdlemg31c  40034  cdlemg35  40048  trlcone  40063  tendoeq2  40109  cdlemj3  40158  cdlemk26b-3  40240  cdlemk33N  40244  cdleml3N  40313  cdlemn  40547  dih1dimb2  40576  dihord5apre  40597  dihmeetlem1N  40625  dihglblem5apreN  40626  dihglblem2N  40629  dihglblem3N  40630  dihmeetlem13N  40654  dihmeetlem15N  40656  dihatexv  40673  hdmap14lem12  41214  uzindd  41309  lcmineqlem1  41361  sticksstones1  41429  metakunt1  41452  metakunt5  41456  frlmfzowrdb  41545  nn0rppwr  41687  nn0expgcd  41689  dvdsexpnn0  41695  rtprmirr  41700  oddcomabszz  42146  jm2.19lem4  42194  fiuneneq  42402  idomsubgmo  42403  omcl2  42546  pwinfi3  42777  gneispa  43344  mnringmulrcld  43450  grumnudlem  43507  ismnushort  43523  binomcxplemnn0  43571  addrcom  43697  int3  43836  suctrALT  44050  suctrALTcf  44146  suctrALT3  44148  chordthmALT  44157  iunconnlem2  44159  stoweidlem26  45201  stoweidlem34  45209  issald  45508  goldbachth  46674  nnsgrp  47014  ply1mulgsumlem1  47229  lubsscl  47755  glbsscl  47756