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 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  1366  mp3an3  1450  3gencl  3535  vtocl3gaf  3593  vtocl3ga  3595  moi  3740  disji  5151  disjord  5155  3optocl  5796  sossfld  6217  f1oresrab  7161  f1cdmsn  7318  soisores  7363  isomin  7373  isofrlem  7376  ovmpos  7598  ov2gf  7599  ndmovord  7640  nnsuc  7921  poxp  8169  frpoins3xp3g  8182  brtpos  8276  dfsmo2  8403  smoiun  8417  smoord  8421  smogt  8423  omeulem1  8638  omeu  8641  oewordi  8647  uniinqs  8855  mapvalg  8894  pmvalg  8895  elmapg  8897  xpdom3  9136  mapdom3  9215  sdomdomtrfi  9267  domsdomtrfi  9268  php  9273  php3  9275  nndomog  9279  php3OLD  9287  onomeneq  9291  sucdom  9298  unxpdomlem3  9315  isinf  9323  isinfOLD  9324  f1finf1o  9333  isfinite2  9362  prfi  9391  ordiso  9585  cnfcom3clem  9774  r111  9844  tskwe  10019  pr2ne  10073  pr2neOLD  10074  infxpenlem  10082  dfac8alem  10098  infdif  10277  infdif2  10278  cff1  10327  coflim  10330  cfslbn  10336  cfslb2n  10337  cofsmo  10338  cfsmolem  10339  cfcoflem  10341  fin23lem27  10397  isf32lem9  10430  isf34lem6  10449  axcc2lem  10505  domtriomlem  10511  axdc4lem  10524  zorn2lem2  10566  axdclem2  10589  konigthlem  10637  gchen1  10694  gchen2  10695  gchpwdom  10739  gchaleph  10740  winainflem  10762  tskcard  10850  gruiun  10868  gruen  10881  intgru  10883  grudomon  10886  grur1a  10888  grutsk1  10890  nqereu  10998  nqereq  11004  ltsonq  11038  prlem934  11102  reclem3pr  11118  1re  11290  axsup  11365  addlid  11473  recex  11922  lemul1a  12148  lt2msq  12180  fimaxre2  12240  zdiv  12713  zextlt  12717  prime  12724  uzind2  12736  fzind  12741  lbzbi  13001  qbtwnxr  13262  qextltlem  13264  xralrple  13267  xltneg  13279  xlt2add  13322  supxrgtmnf  13391  ixxub  13428  ixxlb  13429  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  iocssre  13487  icossre  13488  iccssre  13489  fzen  13601  expclzlem  14134  expaddz  14157  expmulz  14159  hashgadd  14426  hashunsngx  14442  hashgt23el  14473  elovmpowrd  14606  pfxnd0  14736  ccatopth2  14765  pfxccatin12  14781  cshf1  14858  shftuz  15118  cau3lem  15403  caubnd  15407  climuni  15598  lo1resb  15610  o1resb  15612  o1of2  15659  o1add  15660  o1mul  15661  o1sub  15662  ntrivcvgmul  15950  eflt  16165  moddvds  16313  dvdscmulr  16333  dvdsmulcr  16334  dvdsle  16358  divalglem8  16448  divalgb  16452  ndvdssub  16457  bitsfzo  16481  gcdcllem1  16545  gcdcllem3  16547  dvdsgcd  16591  nn0rppwr  16608  nn0expgcd  16611  lcmgcdlem  16653  lcmfeq0b  16677  qredeu  16705  isprm3  16730  prmdvdsexpr  16764  prmexpb  16766  eulerthlem2  16829  fermltl  16831  coprimeprodsq  16855  pythagtrip  16881  pcprendvds  16887  pcpremul  16890  pcdvdsb  16916  pc2dvds  16926  4sqlem12  17003  4sqlem18  17009  vdwlem10  17037  cshwshashlem3  17145  xpsrnbas  17631  ismred  17660  mrieqv2d  17697  iscatd  17731  isfuncd  17929  fthestrcsetc  18219  fthsetcestrc  18234  poslubd  18483  dirtr  18672  mulgaddcom  19138  ghmrn  19269  pmtrprfv3  19496  mndodcongi  19585  oddvdsnn0  19586  oddvds  19589  odcl2  19607  odhash3  19618  gexdvds  19626  pgpfi  19647  lsmss1b  19708  lsmss2b  19710  efgsrel  19776  efgred  19790  cntzcmn  19882  cyggenod  19926  lt6abl  19937  gsumcom2  20017  pgpfac1lem2  20119  pgpfac1lem3  20121  dvdsunit  20405  unitmulclb  20407  irredrmul  20453  isabvd  20835  lmodvsdi  20905  lss0cl  20968  islbs3  21180  lbsextlem2  21184  xrsdsreclblem  21453  psrbaglefi  21969  mvrf1  22029  coe1fzgsumd  22329  gsummoncoe1  22333  evl1gsumd  22382  scmataddcl  22543  scmatsubcl  22544  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  m2cpmrngiso  22785  pm2mpf1  22826  opnnei  23149  neindisj2  23152  cncls2  23302  cncls  23303  cnntr  23304  cnpresti  23317  cnprest  23318  lmcnp  23333  isreg2  23406  ordthauslem  23412  unconn  23458  2ndc1stc  23480  kgen2ss  23584  ptclsg  23644  cnmptcom  23707  kqfvima  23759  hmeof1o  23793  fbncp  23868  fbfinnfr  23870  trfbas2  23872  isufil2  23937  ufprim  23938  trufil  23939  filufint  23949  hausflim  24010  flimrest  24012  flimcls  24014  cnpfcf  24070  alexsubALT  24080  tmdgsum  24124  opnsubg  24137  cldsubg  24140  qustgpopn  24149  tsmsxp  24184  blpnf  24428  blssps  24455  blss  24456  blssec  24466  neibl  24535  prdsxmslem2  24563  xrsmopn  24853  metnrm  24903  climcncf  24945  iccpnfhmeo  24995  xrhmeo  24996  bndth  25009  cphsqrtcl3  25240  iscau2  25330  iscmet3lem2  25345  bcthlem5  25381  bcth3  25384  ishl2  25423  ivthlem1  25505  cmmbl  25588  iundisj2  25603  voliunlem2  25605  mbfaddlem  25714  itg2itg1  25791  itg2seq  25797  itg2mulclem  25801  cnplimc  25942  dvres2  25967  deg1nn0clb  26149  deg1lt0  26150  deg1ge  26157  plypf1  26271  plyadd  26276  plymul  26277  coeeu  26284  dgrub2  26294  coeidlem  26296  coeid3  26299  coemullem  26309  coe11  26312  coemulhi  26313  coemulc  26314  dgreq0  26325  dgrlt  26326  dgradd2  26328  vieta1lem2  26371  tanord1  26597  tanord  26598  logccne0  26638  cxpeq0  26738  cxpmul2z  26751  cxpcn3lem  26808  rtprmirr  26821  relogbzcl  26835  angpieqvd  26892  o1cxp  27036  scvxcvx  27047  chtublem  27273  bposlem3  27348  lgsqr  27413  2sqnn  27501  dchrisumlema  27550  dchrisumlem2  27552  ostth2lem3  27697  nosepon  27728  noextenddif  27731  nolesgn2o  27734  nogesgn1o  27736  nosepne  27743  nodense  27755  tghilberti2  28664  inagswap  28867  f1otrg  28897  brbtwn2  28938  axpasch  28974  axcontlem4  29000  axcontlem5  29001  upgredg2vtx  29176  usgredg2vtxeuALT  29257  sizusglecusg  29499  upgredginwlk  29672  frgrwopreg1  30350  frgrwopreg2  30351  frgrregorufrg  30358  lpni  30512  ipasslem5  30867  htthlem  30949  omlsii  31435  spansni  31589  spansneleq  31602  elspansn4  31605  sumspansn  31681  homco1  31833  homulass  31834  mdsl0  32342  ssdmd1  32345  ssdmd2  32346  cvdmd  32369  chirredlem2  32423  atdmd  32430  atmd2  32432  disjif  32600  iundisj2f  32612  isoun  32713  preiman0  32721  padct  32733  iocinioc2  32784  iundisj2fi  32802  archiabllem1a  33171  archiabllem2a  33174  slmdvsdi  33194  ordtconnlem1  33870  indpi1  33984  measinblem  34184  measres  34186  measdivcstALTV  34189  mbfmco2  34230  orvclteinc  34440  sgn3da  34506  sgnnbi  34510  sgnpbi  34511  bnj605  34883  bnj607  34892  bnj964  34919  bnj1033  34945  bnj1128  34966  bnj1137  34971  bnj1136  34973  bnj1413  35011  bnj60  35038  fineqvac  35073  cusgredgex  35089  subgrwlk  35100  acycgr1v  35117  cvmlift2lem10  35280  msubvrs  35528  wsuclem  35789  dfrdg4  35915  brcolinear2  36022  brsegle2  36073  nn0prpw  36289  ntruni  36293  clsint2  36295  fnessref  36323  fnemeet2  36333  fnejoin2  36335  limsucncmpi  36411  ee7.2aOLD  36427  bj-idreseq  37128  dissneqlem  37306  isbasisrelowllem1  37321  isbasisrelowllem2  37322  icoreclin  37323  poimirlem9  37589  poimirlem30  37610  poimirlem32  37612  areacirc  37673  filbcmb  37700  mettrifi  37717  heiborlem8  37778  heiborlem10  37780  heibor  37781  riscer  37948  igenval2  38026  lshpcmp  38944  eqlkr  39055  lkrlsp2  39059  lkrshp  39061  cvrnbtwn2  39231  cvlexch3  39288  cvlexch4N  39289  cvlatexchb1  39290  cvlsupr3  39300  exatleN  39361  cvratlem  39378  atcvrj2b  39389  cvrat3  39399  cvrat4  39400  athgt  39413  ps-1  39434  ps-2  39435  3atlem5  39444  3at  39447  llnneat  39471  llnmlplnN  39496  lplnneat  39502  lplnnelln  39503  islpln2a  39505  lplnriaN  39507  lplnribN  39508  lplnexllnN  39521  2llnjaN  39523  lvolnle3at  39539  lvolneatN  39545  lvolnelln  39546  lvolnelpln  39547  islvol2aN  39549  dalem62  39691  pmapglb2N  39728  pmapglb2xN  39729  lncmp  39740  paddasslem14  39790  paddasslem15  39791  pmod2iN  39806  hlmod1i  39813  pclfinclN  39907  osumcllem8N  39920  pexmidlem4N  39930  pl42lem1N  39936  pl42lem4N  39939  lhpexle1  39965  lhpexle2lem  39966  lhpmcvr5N  39984  lhpmcvr6N  39985  ltrneq  40106  trlnidatb  40134  cdleme0ex2N  40181  cdleme27a  40324  cdleme17d3  40453  cdlemeg46gfre  40489  cdleme48gfv1  40493  cdlemeg49lebilem  40496  cdlemf2  40519  cdlemf  40520  cdlemfnid  40521  trlord  40526  cdlemg31c  40656  cdlemg35  40670  trlcone  40685  tendoeq2  40731  cdlemj3  40780  cdlemk26b-3  40862  cdlemk33N  40866  cdleml3N  40935  cdlemn  41169  dih1dimb2  41198  dihord5apre  41219  dihmeetlem1N  41247  dihglblem5apreN  41248  dihglblem2N  41251  dihglblem3N  41252  dihmeetlem13N  41276  dihmeetlem15N  41278  dihatexv  41295  hdmap14lem12  41836  uzindd  41933  lcmineqlem1  41986  sticksstones1  42103  metakunt1  42162  metakunt5  42166  dvdsexpnn0  42321  frlmfzowrdb  42459  oddcomabszz  42901  jm2.19lem4  42949  fiuneneq  43153  idomsubgmo  43154  omcl2  43295  pwinfi3  43525  gneispa  44092  mnringmulrcld  44197  grumnudlem  44254  ismnushort  44270  binomcxplemnn0  44318  addrcom  44444  int3  44583  suctrALT  44797  suctrALTcf  44893  suctrALT3  44895  chordthmALT  44904  iunconnlem2  44906  stoweidlem26  45947  stoweidlem34  45955  issald  46254  goldbachth  47421  grlimgrtri  47820  nnsgrp  47900  ply1mulgsumlem1  48115  lubsscl  48640  glbsscl  48641