Theorem 3expia 1121

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 1120	. 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant125  1368  mp3an3  1452  3gencl  3488  vtocl3gaf  3544  vtocl3ga  3546  moi  3686  disji  5087  disjord  5091  3optocl  5727  sossfld  6147  f1oresrab  7081  f1cdmsn  7239  soisores  7284  isomin  7294  isofrlem  7297  ovmpos  7517  ov2gf  7518  ndmovord  7559  nnsuc  7840  poxp  8084  frpoins3xp3g  8097  brtpos  8191  dfsmo2  8293  smoiun  8307  smoord  8311  smogt  8313  omeulem1  8523  omeu  8526  oewordi  8532  uniinqs  8747  mapvalg  8786  pmvalg  8787  elmapg  8789  xpdom3  9016  mapdom3  9090  sdomdomtrfi  9142  domsdomtrfi  9143  php  9148  php3  9150  nndomog  9154  onomeneq  9155  sucdom  9160  unxpdomlem3  9175  isinf  9183  isinfOLD  9184  f1finf1o  9192  isfinite2  9221  prfi  9250  ordiso  9445  cnfcom3clem  9634  r111  9704  tskwe  9879  pr2ne  9933  pr2neOLD  9934  infxpenlem  9942  dfac8alem  9958  infdif  10137  infdif2  10138  cff1  10187  coflim  10190  cfslbn  10196  cfslb2n  10197  cofsmo  10198  cfsmolem  10199  cfcoflem  10201  fin23lem27  10257  isf32lem9  10290  isf34lem6  10309  axcc2lem  10365  domtriomlem  10371  axdc4lem  10384  zorn2lem2  10426  axdclem2  10449  konigthlem  10497  gchen1  10554  gchen2  10555  gchpwdom  10599  gchaleph  10600  winainflem  10622  tskcard  10710  gruiun  10728  gruen  10741  intgru  10743  grudomon  10746  grur1a  10748  grutsk1  10750  nqereu  10858  nqereq  10864  ltsonq  10898  prlem934  10962  reclem3pr  10978  1re  11150  axsup  11225  addlid  11333  recex  11786  lemul1a  12012  lt2msq  12044  fimaxre2  12104  zdiv  12580  zextlt  12584  prime  12591  uzind2  12603  fzind  12608  lbzbi  12871  qbtwnxr  13136  qextltlem  13138  xralrple  13141  xltneg  13153  xlt2add  13196  supxrgtmnf  13265  ixxub  13303  ixxlb  13304  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  iocssre  13364  icossre  13365  iccssre  13366  fzen  13478  expclzlem  14024  expaddz  14047  expmulz  14049  hashgadd  14318  hashunsngx  14334  hashgt23el  14365  elovmpowrd  14499  pfxnd0  14629  ccatopth2  14658  pfxccatin12  14674  cshf1  14751  shftuz  15011  cau3lem  15297  caubnd  15301  climuni  15494  lo1resb  15506  o1resb  15508  o1of2  15555  o1add  15556  o1mul  15557  o1sub  15558  ntrivcvgmul  15844  eflt  16061  moddvds  16209  dvdscmulr  16230  dvdsmulcr  16231  dvdsle  16256  divalglem8  16346  divalgb  16350  ndvdssub  16355  bitsfzo  16381  gcdcllem1  16445  gcdcllem3  16447  dvdsgcd  16490  nn0rppwr  16507  nn0expgcd  16510  lcmgcdlem  16552  lcmfeq0b  16576  qredeu  16604  isprm3  16629  prmdvdsexpr  16663  prmexpb  16665  eulerthlem2  16728  fermltl  16730  coprimeprodsq  16755  pythagtrip  16781  pcprendvds  16787  pcpremul  16790  pcdvdsb  16816  pc2dvds  16826  4sqlem12  16903  4sqlem18  16909  vdwlem10  16937  cshwshashlem3  17044  xpsrnbas  17510  ismred  17539  mrieqv2d  17576  iscatd  17610  isfuncd  17803  fthestrcsetc  18087  fthsetcestrc  18102  poslubd  18348  dirtr  18537  mulgaddcom  19006  ghmrn  19137  pmtrprfv3  19360  mndodcongi  19449  oddvdsnn0  19450  oddvds  19453  odcl2  19471  odhash3  19482  gexdvds  19490  pgpfi  19511  lsmss1b  19572  lsmss2b  19574  efgsrel  19640  efgred  19654  cntzcmn  19746  cyggenod  19790  lt6abl  19801  gsumcom2  19881  pgpfac1lem2  19983  pgpfac1lem3  19985  dvdsunit  20264  unitmulclb  20266  irredrmul  20312  isabvd  20697  lmodvsdi  20767  lss0cl  20829  islbs3  21041  lbsextlem2  21045  xrsdsreclblem  21305  psrbaglefi  21811  mvrf1  21871  coe1fzgsumd  22167  gsummoncoe1  22171  evl1gsumd  22220  scmataddcl  22379  scmatsubcl  22380  mdetunilem9  22483  mdetuni0  22484  mdetmul  22486  m2cpmrngiso  22621  pm2mpf1  22662  opnnei  22983  neindisj2  22986  cncls2  23136  cncls  23137  cnntr  23138  cnpresti  23151  cnprest  23152  lmcnp  23167  isreg2  23240  ordthauslem  23246  unconn  23292  2ndc1stc  23314  kgen2ss  23418  ptclsg  23478  cnmptcom  23541  kqfvima  23593  hmeof1o  23627  fbncp  23702  fbfinnfr  23704  trfbas2  23706  isufil2  23771  ufprim  23772  trufil  23773  filufint  23783  hausflim  23844  flimrest  23846  flimcls  23848  cnpfcf  23904  alexsubALT  23914  tmdgsum  23958  opnsubg  23971  cldsubg  23974  qustgpopn  23983  tsmsxp  24018  blpnf  24261  blssps  24288  blss  24289  blssec  24299  neibl  24365  prdsxmslem2  24393  xrsmopn  24677  metnrm  24727  climcncf  24769  iccpnfhmeo  24819  xrhmeo  24820  bndth  24833  cphsqrtcl3  25063  iscau2  25153  iscmet3lem2  25168  bcthlem5  25204  bcth3  25207  ishl2  25246  ivthlem1  25328  cmmbl  25411  iundisj2  25426  voliunlem2  25428  mbfaddlem  25537  itg2itg1  25613  itg2seq  25619  itg2mulclem  25623  cnplimc  25764  dvres2  25789  deg1nn0clb  25971  deg1lt0  25972  deg1ge  25979  plypf1  26093  plyadd  26098  plymul  26099  coeeu  26106  dgrub2  26116  coeidlem  26118  coeid3  26121  coemullem  26131  coe11  26134  coemulhi  26135  coemulc  26136  dgreq0  26147  dgrlt  26148  dgradd2  26150  vieta1lem2  26195  tanord1  26422  tanord  26423  logccne0  26463  cxpeq0  26563  cxpmul2z  26576  cxpcn3lem  26633  rtprmirr  26646  relogbzcl  26660  angpieqvd  26717  o1cxp  26861  scvxcvx  26872  chtublem  27098  bposlem3  27173  lgsqr  27238  2sqnn  27326  dchrisumlema  27375  dchrisumlem2  27377  ostth2lem3  27522  nosepon  27553  noextenddif  27556  nolesgn2o  27559  nogesgn1o  27561  nosepne  27568  nodense  27580  onnolt  28143  onslt  28144  onsiso  28145  bdayn0p1  28234  bdayn0sf1o  28235  tghilberti2  28541  inagswap  28744  f1otrg  28774  brbtwn2  28808  axpasch  28844  axcontlem4  28870  axcontlem5  28871  upgredg2vtx  29044  usgredg2vtxeuALT  29125  sizusglecusg  29367  upgredginwlk  29539  frgrwopreg1  30220  frgrwopreg2  30221  frgrregorufrg  30228  lpni  30382  ipasslem5  30737  htthlem  30819  omlsii  31305  spansni  31459  spansneleq  31472  elspansn4  31475  sumspansn  31551  homco1  31703  homulass  31704  mdsl0  32212  ssdmd1  32215  ssdmd2  32216  cvdmd  32239  chirredlem2  32293  atdmd  32300  atmd2  32302  disjif  32480  iundisj2f  32492  isoun  32598  preiman0  32606  padct  32616  iocinioc2  32675  iundisj2fi  32693  sgn3da  32732  sgnnbi  32736  sgnpbi  32737  indpi1  32756  archiabllem1a  33118  archiabllem2a  33121  slmdvsdi  33141  ordtconnlem1  33887  measinblem  34183  measres  34185  measdivcstALTV  34188  mbfmco2  34229  orvclteinc  34440  bnj605  34870  bnj607  34879  bnj964  34906  bnj1033  34932  bnj1128  34953  bnj1137  34958  bnj1136  34960  bnj1413  34998  bnj60  35025  fineqvac  35060  cusgredgex  35082  subgrwlk  35092  acycgr1v  35109  cvmlift2lem10  35272  msubvrs  35520  wsuclem  35786  dfrdg4  35912  brcolinear2  36019  brsegle2  36070  nn0prpw  36284  ntruni  36288  clsint2  36290  fnessref  36318  fnemeet2  36328  fnejoin2  36330  limsucncmpi  36406  ee7.2aOLD  36422  bj-idreseq  37123  dissneqlem  37301  isbasisrelowllem1  37316  isbasisrelowllem2  37317  icoreclin  37318  poimirlem9  37596  poimirlem30  37617  poimirlem32  37619  areacirc  37680  filbcmb  37707  mettrifi  37724  heiborlem8  37785  heiborlem10  37787  heibor  37788  riscer  37955  igenval2  38033  lshpcmp  38954  eqlkr  39065  lkrlsp2  39069  lkrshp  39071  cvrnbtwn2  39241  cvlexch3  39298  cvlexch4N  39299  cvlatexchb1  39300  cvlsupr3  39310  exatleN  39371  cvratlem  39388  atcvrj2b  39399  cvrat3  39409  cvrat4  39410  athgt  39423  ps-1  39444  ps-2  39445  3atlem5  39454  3at  39457  llnneat  39481  llnmlplnN  39506  lplnneat  39512  lplnnelln  39513  islpln2a  39515  lplnriaN  39517  lplnribN  39518  lplnexllnN  39531  2llnjaN  39533  lvolnle3at  39549  lvolneatN  39555  lvolnelln  39556  lvolnelpln  39557  islvol2aN  39559  dalem62  39701  pmapglb2N  39738  pmapglb2xN  39739  lncmp  39750  paddasslem14  39800  paddasslem15  39801  pmod2iN  39816  hlmod1i  39823  pclfinclN  39917  osumcllem8N  39930  pexmidlem4N  39940  pl42lem1N  39946  pl42lem4N  39949  lhpexle1  39975  lhpexle2lem  39976  lhpmcvr5N  39994  lhpmcvr6N  39995  ltrneq  40116  trlnidatb  40144  cdleme0ex2N  40191  cdleme27a  40334  cdleme17d3  40463  cdlemeg46gfre  40499  cdleme48gfv1  40503  cdlemeg49lebilem  40506  cdlemf2  40529  cdlemf  40530  cdlemfnid  40531  trlord  40536  cdlemg31c  40666  cdlemg35  40680  trlcone  40695  tendoeq2  40741  cdlemj3  40790  cdlemk26b-3  40872  cdlemk33N  40876  cdleml3N  40945  cdlemn  41179  dih1dimb2  41208  dihord5apre  41229  dihmeetlem1N  41257  dihglblem5apreN  41258  dihglblem2N  41261  dihglblem3N  41262  dihmeetlem13N  41286  dihmeetlem15N  41288  dihatexv  41305  hdmap14lem12  41846  uzindd  41938  lcmineqlem1  41990  sticksstones1  42107  dvdsexpnn0  42295  frlmfzowrdb  42465  oddcomabszz  42906  jm2.19lem4  42954  fiuneneq  43154  idomsubgmo  43155  omcl2  43295  pwinfi3  43525  gneispa  44092  mnringmulrcld  44190  grumnudlem  44247  ismnushort  44263  binomcxplemnn0  44311  addrcom  44437  int3  44575  suctrALT  44788  suctrALTcf  44884  suctrALT3  44886  chordthmALT  44895  iunconnlem2  44897  relpmin  44915  relpfrlem  44916  stoweidlem26  45997  stoweidlem34  46005  issald  46304  goldbachth  47521  grlimgrtri  47968  nnsgrp  48138  ply1mulgsumlem1  48348  lubsscl  48921  glbsscl  48922