Theorem 3expia 1137

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ad5ant125OLD  1389  mp3an3  1476  3gencl  3506  vtocl3gaf  3553  vtocl3ga  3554  moi  3690  disji  5095  disjord  5099  3optocl  5756  sossfld  6182  f1oresrab  7121  f1cdmsn  7278  soisores  7323  isomin  7333  isofrlem  7336  ovmpos  7556  ov2gf  7557  ndmovord  7598  nnsuc  7876  poxp  8120  frpoins3xp3g  8133  brtpos  8227  dfsmo2  8330  smoiun  8344  smoord  8348  smogt  8350  omeulem1  8563  omeu  8566  oewordi  8573  uniinqs  8791  mapvalg  8829  pmvalg  8830  elmapg  8832  xpdom3  9059  mapdom3  9133  sdomdomtrfi  9181  domsdomtrfi  9182  php  9187  php3  9189  nndomog  9193  onomeneq  9194  sucdom  9200  unxpdomlem3  9214  isinf  9221  f1finf1o  9229  isfinite2  9254  prfi  9279  ordiso  9474  cnfcom3clem  9670  r111  9743  tskwe  9932  pr2ne  9985  infxpenlem  9993  dfac8alem  10009  infdif  10187  infdif2  10188  cff1  10238  coflim  10241  cfslbn  10247  cfslb2n  10248  cofsmo  10249  cfsmolem  10250  cfcoflem  10252  fin23lem27  10308  isf32lem9  10341  isf34lem6  10360  axcc2lem  10416  domtriomlem  10422  axdc4lem  10435  zorn2lem2  10477  axdclem2  10500  konigthlem  10549  gchen1  10606  gchen2  10607  gchpwdom  10651  gchaleph  10652  winainflem  10674  tskcard  10762  gruiun  10780  gruen  10793  intgru  10795  grudomon  10798  grur1a  10800  grutsk1  10802  nqereu  10910  nqereq  10916  ltsonq  10950  prlem934  11014  reclem3pr  11030  1re  11204  axsup  11281  addlid  11389  recex  11842  lemul1a  12065  lt2msq  12096  fimaxre2  12156  indpi1  12228  zdiv  12662  zextlt  12666  prime  12673  uzind2  12685  fzind  12690  lbzbi  12956  qbtwnxr  13222  qextltlem  13224  xralrple  13227  xltneg  13239  xlt2add  13282  supxrgtmnf  13351  ixxub  13389  ixxlb  13390  ioo0  13393  ico0  13414  ioc0  13415  icc0  13416  iocssre  13450  icossre  13451  iccssre  13452  fzen  13565  expclzlem  14115  expaddz  14138  expmulz  14140  hashgadd  14409  hashunsngx  14425  hashgt23el  14457  elovmpowrd  14591  pfxnd0  14722  ccatopth2  14750  pfxccatin12  14766  cshf1  14843  shftuz  15102  sgn3da  15134  sgnnbi  15137  sgnpbi  15138  cau3lem  15402  caubnd  15406  climuni  15599  lo1resb  15611  o1resb  15613  o1of2  15660  o1add  15661  o1mul  15662  o1sub  15663  ntrivcvgmul  15952  eflt  16169  moddvds  16317  dvdscmulr  16338  dvdsmulcr  16339  dvdsle  16364  divalglem8  16454  divalgb  16458  ndvdssub  16463  bitsfzo  16489  gcdcllem1  16553  gcdcllem3  16555  dvdsgcd  16598  nn0rppwr  16615  nn0expgcd  16618  lcmgcdlem  16660  lcmfeq0b  16684  qredeu  16712  isprm3  16737  prmdvdsexpr  16772  prmexpb  16774  eulerthlem2  16837  fermltl  16839  coprimeprodsq  16864  pythagtrip  16890  pcprendvds  16896  pcpremul  16899  pcdvdsb  16925  pc2dvds  16935  4sqlem12  17012  4sqlem18  17018  vdwlem10  17046  cshwshashlem3  17153  xpsrnbas  17621  ismred  17650  mrieqv2d  17691  iscatd  17725  isfuncd  17918  fthestrcsetc  18202  fthsetcestrc  18217  poslubd  18463  dirtr  18654  mulgaddcom  19160  ghmrn  19295  pmtrprfv3  19520  mndodcongi  19609  oddvdsnn0  19610  oddvds  19613  odcl2  19631  odhash3  19642  gexdvds  19650  pgpfi  19671  lsmss1b  19732  lsmss2b  19734  efgsrel  19800  efgred  19814  cntzcmn  19906  cyggenod  19950  lt6abl  19961  gsumcom2  20041  pgpfac1lem2  20143  pgpfac1lem3  20145  dvdsunit  20457  unitmulclb  20459  irredrmul  20505  isabvd  20889  lmodvsdi  20980  lss0cl  21042  islbs3  21253  lbsextlem2  21257  xrsdsreclblem  21528  psrbaglefi  22041  mvrf1  22100  coe1fzgsumd  22429  gsummoncoe1  22433  evl1gsumd  22482  scmataddcl  22638  scmatsubcl  22639  mdetunilem9  22742  mdetuni0  22743  mdetmul  22745  m2cpmrngiso  22880  pm2mpf1  22921  opnnei  23242  neindisj2  23245  cncls2  23395  cncls  23396  cnntr  23397  cnpresti  23410  cnprest  23411  lmcnp  23426  isreg2  23499  ordthauslem  23505  unconn  23551  2ndc1stc  23573  kgen2ss  23677  ptclsg  23737  cnmptcom  23800  kqfvima  23852  hmeof1o  23886  fbncp  23961  fbfinnfr  23963  trfbas2  23965  isufil2  24030  ufprim  24031  trufil  24032  filufint  24042  hausflim  24103  flimrest  24105  flimcls  24107  cnpfcf  24163  alexsubALT  24173  tmdgsum  24217  opnsubg  24230  cldsubg  24233  qustgpopn  24242  tsmsxp  24277  blpnf  24519  blssps  24546  blss  24547  blssec  24557  neibl  24623  prdsxmslem2  24651  xrsmopn  24935  metnrm  24985  climcncf  25024  iccpnfhmeo  25069  xrhmeo  25070  bndth  25082  cphsqrtcl3  25311  iscau2  25401  iscmet3lem2  25416  bcthlem5  25452  bcth3  25455  ishl2  25494  ivthlem1  25575  cmmbl  25658  iundisj2  25673  voliunlem2  25675  mbfaddlem  25784  itg2itg1  25860  itg2seq  25866  itg2mulclem  25870  cnplimc  26011  dvres2  26036  deg1nn0clb  26212  deg1lt0  26213  deg1ge  26220  plypf1  26334  plyadd  26339  plymul  26340  coeeu  26347  dgrub2  26357  coeidlem  26359  coeid3  26362  coemullem  26372  coe11  26375  coemulhi  26376  coemulc  26377  dgreq0  26387  dgrlt  26388  dgradd2  26390  vieta1lem2  26437  tanord1  26664  tanord  26665  logccne0  26705  cxpeq0  26805  cxpmul2z  26818  cxpcn3lem  26874  rtprmirr  26887  relogbzcl  26901  angpieqvd  26958  o1cxp  27101  scvxcvx  27112  chtublem  27337  bposlem3  27412  lgsqr  27477  2sqnn  27565  dchrisumlema  27614  dchrisumlem2  27616  ostth2lem3  27761  nosepon  27791  noextenddif  27794  nolesgn2o  27797  nogesgn1o  27799  nosepne  27806  nodense  27818  onnolt  28421  onlts  28422  oniso  28426  bdayn0p1  28524  bdayn0sf1o  28525  tghilberti2  28869  inagswap  29109  f1otrg  29157  brbtwn2  29192  axpasch  29228  axcontlem4  29254  axcontlem5  29255  upgredg2vtx  29428  usgredg2vtxeuALT  29509  sizusglecusg  29750  upgredginwlk  29922  frgrwopreg1  30606  frgrwopreg2  30607  frgrregorufrg  30614  lpni  30769  ipasslem5  31124  htthlem  31206  omlsii  31692  spansni  31846  spansneleq  31859  elspansn4  31862  sumspansn  31938  homco1  32090  homulass  32091  mdsl0  32599  ssdmd1  32602  ssdmd2  32603  cvdmd  32626  chirredlem2  32680  atdmd  32687  atmd2  32689  disjif  32860  iundisj2f  32872  isoun  32984  preiman0  32992  padct  33000  iocinioc2  33061  iundisj2fi  33079  archiabllem1a  33448  archiabllem2a  33451  slmdvsdi  33472  ordtconnlem1  34255  measinblem  34551  measres  34553  measdivcstALTV  34556  mbfmco2  34596  orvclteinc  34807  bnj605  35236  bnj607  35245  bnj964  35272  bnj1033  35298  bnj1128  35319  bnj1137  35324  bnj1136  35326  bnj1413  35364  bnj60  35391  rankfilimb  35434  r1filim  35436  fineqvac  35448  fineqvnttrclselem3  35455  fineqvnttrclse  35456  vonf1oonfo  35494  cusgredgex  35509  subgrwlk  35519  acycgr1v  35536  cvmlift2lem10  35699  msubvrs  35947  wsuclem  36210  dfrdg4  36338  brcolinear2  36445  brsegle2  36496  nn0prpw  36719  ntruni  36723  clsint2  36725  fnessref  36753  fnemeet2  36763  fnejoin2  36765  limsucncmpi  36841  ee7.2aOLD  36857  bj-idreseq  37689  dissneqlem  37869  isbasisrelowllem1  37884  isbasisrelowllem2  37885  icoreclin  37886  poimirlem9  38163  poimirlem30  38184  poimirlem32  38186  areacirc  38247  filbcmb  38274  mettrifi  38291  heiborlem8  38352  heiborlem10  38354  heibor  38355  riscer  38522  igenval2  38600  eldisjim3  39349  eldisjs6  39474  lshpcmp  39647  eqlkr  39758  lkrlsp2  39762  lkrshp  39764  cvrnbtwn2  39934  cvlexch3  39991  cvlexch4N  39992  cvlatexchb1  39993  cvlsupr3  40003  exatleN  40063  cvratlem  40080  atcvrj2b  40091  cvrat3  40101  cvrat4  40102  athgt  40115  ps-1  40136  ps-2  40137  3atlem5  40146  3at  40149  llnneat  40173  llnmlplnN  40198  lplnneat  40204  lplnnelln  40205  islpln2a  40207  lplnriaN  40209  lplnribN  40210  lplnexllnN  40223  2llnjaN  40225  lvolnle3at  40241  lvolneatN  40247  lvolnelln  40248  lvolnelpln  40249  islvol2aN  40251  dalem62  40393  pmapglb2N  40430  pmapglb2xN  40431  lncmp  40442  paddasslem14  40492  paddasslem15  40493  pmod2iN  40508  hlmod1i  40515  pclfinclN  40609  osumcllem8N  40622  pexmidlem4N  40632  pl42lem1N  40638  pl42lem4N  40641  lhpexle1  40667  lhpexle2lem  40668  lhpmcvr5N  40686  lhpmcvr6N  40687  ltrneq  40808  trlnidatb  40836  cdleme0ex2N  40883  cdleme27a  41026  cdleme17d3  41155  cdlemeg46gfre  41191  cdleme48gfv1  41195  cdlemeg49lebilem  41198  cdlemf2  41221  cdlemf  41222  cdlemfnid  41223  trlord  41228  cdlemg31c  41358  cdlemg35  41372  trlcone  41387  tendoeq2  41433  cdlemj3  41482  cdlemk26b-3  41564  cdlemk33N  41568  cdleml3N  41637  cdlemn  41871  dih1dimb2  41900  dihord5apre  41921  dihmeetlem1N  41949  dihglblem5apreN  41950  dihglblem2N  41953  dihglblem3N  41954  dihmeetlem13N  41978  dihmeetlem15N  41980  dihatexv  41997  hdmap14lem12  42538  uzindd  42630  lcmineqlem1  42681  sticksstones1  42798  dvdsexpnn0  42980  frlmfzowrdb  43163  oddcomabszz  43558  jm2.19lem4  43606  fiuneneq  43806  idomsubgmo  43807  omcl2  43947  pwinfi3  44176  gneispa  44743  mnringmulrcld  44839  grumnudlem  44882  ismnushort  44898  binomcxplemnn0  44946  addrcom  45070  int3  45208  suctrALT  45421  suctrALTcf  45517  suctrALT3  45519  chordthmALT  45528  iunconnlem2  45530  relpmin  45548  relpfrlem  45549  stoweidlem26  46627  stoweidlem34  46635  issald  46934  goldbachth  48183  nprmdvdsfacm1  48260  grlimgrtri  48652  nnsgrp  48826  ply1mulgsumlem1  49046  lubsscl  49618  glbsscl  49619