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  3491  vtocl3gaf  3547  vtocl3ga  3549  moi  3689  disji  5092  disjord  5096  3optocl  5735  sossfld  6159  f1oresrab  7099  f1cdmsn  7257  soisores  7302  isomin  7312  isofrlem  7315  ovmpos  7537  ov2gf  7538  ndmovord  7579  nnsuc  7860  poxp  8107  frpoins3xp3g  8120  brtpos  8214  dfsmo2  8316  smoiun  8330  smoord  8334  smogt  8336  omeulem1  8546  omeu  8549  oewordi  8555  uniinqs  8770  mapvalg  8809  pmvalg  8810  elmapg  8812  xpdom3  9039  mapdom3  9113  sdomdomtrfi  9165  domsdomtrfi  9166  php  9171  php3  9173  nndomog  9177  onomeneq  9178  sucdom  9183  unxpdomlem3  9199  isinf  9207  isinfOLD  9208  f1finf1o  9216  isfinite2  9245  prfi  9274  ordiso  9469  cnfcom3clem  9658  r111  9728  tskwe  9903  pr2ne  9957  pr2neOLD  9958  infxpenlem  9966  dfac8alem  9982  infdif  10161  infdif2  10162  cff1  10211  coflim  10214  cfslbn  10220  cfslb2n  10221  cofsmo  10222  cfsmolem  10223  cfcoflem  10225  fin23lem27  10281  isf32lem9  10314  isf34lem6  10333  axcc2lem  10389  domtriomlem  10395  axdc4lem  10408  zorn2lem2  10450  axdclem2  10473  konigthlem  10521  gchen1  10578  gchen2  10579  gchpwdom  10623  gchaleph  10624  winainflem  10646  tskcard  10734  gruiun  10752  gruen  10765  intgru  10767  grudomon  10770  grur1a  10772  grutsk1  10774  nqereu  10882  nqereq  10888  ltsonq  10922  prlem934  10986  reclem3pr  11002  1re  11174  axsup  11249  addlid  11357  recex  11810  lemul1a  12036  lt2msq  12068  fimaxre2  12128  zdiv  12604  zextlt  12608  prime  12615  uzind2  12627  fzind  12632  lbzbi  12895  qbtwnxr  13160  qextltlem  13162  xralrple  13165  xltneg  13177  xlt2add  13220  supxrgtmnf  13289  ixxub  13327  ixxlb  13328  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  iocssre  13388  icossre  13389  iccssre  13390  fzen  13502  expclzlem  14048  expaddz  14071  expmulz  14073  hashgadd  14342  hashunsngx  14358  hashgt23el  14389  elovmpowrd  14523  pfxnd0  14653  ccatopth2  14682  pfxccatin12  14698  cshf1  14775  shftuz  15035  cau3lem  15321  caubnd  15325  climuni  15518  lo1resb  15530  o1resb  15532  o1of2  15579  o1add  15580  o1mul  15581  o1sub  15582  ntrivcvgmul  15868  eflt  16085  moddvds  16233  dvdscmulr  16254  dvdsmulcr  16255  dvdsle  16280  divalglem8  16370  divalgb  16374  ndvdssub  16379  bitsfzo  16405  gcdcllem1  16469  gcdcllem3  16471  dvdsgcd  16514  nn0rppwr  16531  nn0expgcd  16534  lcmgcdlem  16576  lcmfeq0b  16600  qredeu  16628  isprm3  16653  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  17534  ismred  17563  mrieqv2d  17600  iscatd  17634  isfuncd  17827  fthestrcsetc  18111  fthsetcestrc  18126  poslubd  18372  dirtr  18561  mulgaddcom  19030  ghmrn  19161  pmtrprfv3  19384  mndodcongi  19473  oddvdsnn0  19474  oddvds  19477  odcl2  19495  odhash3  19506  gexdvds  19514  pgpfi  19535  lsmss1b  19596  lsmss2b  19598  efgsrel  19664  efgred  19678  cntzcmn  19770  cyggenod  19814  lt6abl  19825  gsumcom2  19905  pgpfac1lem2  20007  pgpfac1lem3  20009  dvdsunit  20288  unitmulclb  20290  irredrmul  20336  isabvd  20721  lmodvsdi  20791  lss0cl  20853  islbs3  21065  lbsextlem2  21069  xrsdsreclblem  21329  psrbaglefi  21835  mvrf1  21895  coe1fzgsumd  22191  gsummoncoe1  22195  evl1gsumd  22244  scmataddcl  22403  scmatsubcl  22404  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  m2cpmrngiso  22645  pm2mpf1  22686  opnnei  23007  neindisj2  23010  cncls2  23160  cncls  23161  cnntr  23162  cnpresti  23175  cnprest  23176  lmcnp  23191  isreg2  23264  ordthauslem  23270  unconn  23316  2ndc1stc  23338  kgen2ss  23442  ptclsg  23502  cnmptcom  23565  kqfvima  23617  hmeof1o  23651  fbncp  23726  fbfinnfr  23728  trfbas2  23730  isufil2  23795  ufprim  23796  trufil  23797  filufint  23807  hausflim  23868  flimrest  23870  flimcls  23872  cnpfcf  23928  alexsubALT  23938  tmdgsum  23982  opnsubg  23995  cldsubg  23998  qustgpopn  24007  tsmsxp  24042  blpnf  24285  blssps  24312  blss  24313  blssec  24323  neibl  24389  prdsxmslem2  24417  xrsmopn  24701  metnrm  24751  climcncf  24793  iccpnfhmeo  24843  xrhmeo  24844  bndth  24857  cphsqrtcl3  25087  iscau2  25177  iscmet3lem2  25192  bcthlem5  25228  bcth3  25231  ishl2  25270  ivthlem1  25352  cmmbl  25435  iundisj2  25450  voliunlem2  25452  mbfaddlem  25561  itg2itg1  25637  itg2seq  25643  itg2mulclem  25647  cnplimc  25788  dvres2  25813  deg1nn0clb  25995  deg1lt0  25996  deg1ge  26003  plypf1  26117  plyadd  26122  plymul  26123  coeeu  26130  dgrub2  26140  coeidlem  26142  coeid3  26145  coemullem  26155  coe11  26158  coemulhi  26159  coemulc  26160  dgreq0  26171  dgrlt  26172  dgradd2  26174  vieta1lem2  26219  tanord1  26446  tanord  26447  logccne0  26487  cxpeq0  26587  cxpmul2z  26600  cxpcn3lem  26657  rtprmirr  26670  relogbzcl  26684  angpieqvd  26741  o1cxp  26885  scvxcvx  26896  chtublem  27122  bposlem3  27197  lgsqr  27262  2sqnn  27350  dchrisumlema  27399  dchrisumlem2  27401  ostth2lem3  27546  nosepon  27577  noextenddif  27580  nolesgn2o  27583  nogesgn1o  27585  nosepne  27592  nodense  27604  onnolt  28167  onslt  28168  onsiso  28169  bdayn0p1  28258  bdayn0sf1o  28259  tghilberti2  28565  inagswap  28768  f1otrg  28798  brbtwn2  28832  axpasch  28868  axcontlem4  28894  axcontlem5  28895  upgredg2vtx  29068  usgredg2vtxeuALT  29149  sizusglecusg  29391  upgredginwlk  29564  frgrwopreg1  30247  frgrwopreg2  30248  frgrregorufrg  30255  lpni  30409  ipasslem5  30764  htthlem  30846  omlsii  31332  spansni  31486  spansneleq  31499  elspansn4  31502  sumspansn  31578  homco1  31730  homulass  31731  mdsl0  32239  ssdmd1  32242  ssdmd2  32243  cvdmd  32266  chirredlem2  32320  atdmd  32327  atmd2  32329  disjif  32507  iundisj2f  32519  isoun  32625  preiman0  32633  padct  32643  iocinioc2  32702  iundisj2fi  32720  sgn3da  32759  sgnnbi  32763  sgnpbi  32764  indpi1  32783  archiabllem1a  33145  archiabllem2a  33148  slmdvsdi  33168  ordtconnlem1  33914  measinblem  34210  measres  34212  measdivcstALTV  34215  mbfmco2  34256  orvclteinc  34467  bnj605  34897  bnj607  34906  bnj964  34933  bnj1033  34959  bnj1128  34980  bnj1137  34985  bnj1136  34987  bnj1413  35025  bnj60  35052  fineqvac  35087  cusgredgex  35109  subgrwlk  35119  acycgr1v  35136  cvmlift2lem10  35299  msubvrs  35547  wsuclem  35813  dfrdg4  35939  brcolinear2  36046  brsegle2  36097  nn0prpw  36311  ntruni  36315  clsint2  36317  fnessref  36345  fnemeet2  36355  fnejoin2  36357  limsucncmpi  36433  ee7.2aOLD  36449  bj-idreseq  37150  dissneqlem  37328  isbasisrelowllem1  37343  isbasisrelowllem2  37344  icoreclin  37345  poimirlem9  37623  poimirlem30  37644  poimirlem32  37646  areacirc  37707  filbcmb  37734  mettrifi  37751  heiborlem8  37812  heiborlem10  37814  heibor  37815  riscer  37982  igenval2  38060  lshpcmp  38981  eqlkr  39092  lkrlsp2  39096  lkrshp  39098  cvrnbtwn2  39268  cvlexch3  39325  cvlexch4N  39326  cvlatexchb1  39327  cvlsupr3  39337  exatleN  39398  cvratlem  39415  atcvrj2b  39426  cvrat3  39436  cvrat4  39437  athgt  39450  ps-1  39471  ps-2  39472  3atlem5  39481  3at  39484  llnneat  39508  llnmlplnN  39533  lplnneat  39539  lplnnelln  39540  islpln2a  39542  lplnriaN  39544  lplnribN  39545  lplnexllnN  39558  2llnjaN  39560  lvolnle3at  39576  lvolneatN  39582  lvolnelln  39583  lvolnelpln  39584  islvol2aN  39586  dalem62  39728  pmapglb2N  39765  pmapglb2xN  39766  lncmp  39777  paddasslem14  39827  paddasslem15  39828  pmod2iN  39843  hlmod1i  39850  pclfinclN  39944  osumcllem8N  39957  pexmidlem4N  39967  pl42lem1N  39973  pl42lem4N  39976  lhpexle1  40002  lhpexle2lem  40003  lhpmcvr5N  40021  lhpmcvr6N  40022  ltrneq  40143  trlnidatb  40171  cdleme0ex2N  40218  cdleme27a  40361  cdleme17d3  40490  cdlemeg46gfre  40526  cdleme48gfv1  40530  cdlemeg49lebilem  40533  cdlemf2  40556  cdlemf  40557  cdlemfnid  40558  trlord  40563  cdlemg31c  40693  cdlemg35  40707  trlcone  40722  tendoeq2  40768  cdlemj3  40817  cdlemk26b-3  40899  cdlemk33N  40903  cdleml3N  40972  cdlemn  41206  dih1dimb2  41235  dihord5apre  41256  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem2N  41288  dihglblem3N  41289  dihmeetlem13N  41313  dihmeetlem15N  41315  dihatexv  41332  hdmap14lem12  41873  uzindd  41965  lcmineqlem1  42017  sticksstones1  42134  dvdsexpnn0  42322  frlmfzowrdb  42492  oddcomabszz  42933  jm2.19lem4  42981  fiuneneq  43181  idomsubgmo  43182  omcl2  43322  pwinfi3  43552  gneispa  44119  mnringmulrcld  44217  grumnudlem  44274  ismnushort  44290  binomcxplemnn0  44338  addrcom  44464  int3  44602  suctrALT  44815  suctrALTcf  44911  suctrALT3  44913  chordthmALT  44922  iunconnlem2  44924  relpmin  44942  relpfrlem  44943  stoweidlem26  46024  stoweidlem34  46032  issald  46331  goldbachth  47548  grlimgrtri  47995  nnsgrp  48165  ply1mulgsumlem1  48375  lubsscl  48948  glbsscl  48949